COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Examples of call-by-name recursion counters.
C00004 ENDMK
C⊗;
Examples of call-by-name recursion counters.

There are two schemes: one by McCarthy and the other independently
devised by Cartwright and Moszkowski.

Mccarthy scheme

let

	%2morris(x,y) ← qif x equal 0 qthen 0 qelse morris(x-1,morris(x,y))%1.

We have

	%2cm(x,y) ← qif x equal 0 qthen 0 qelse cm(x - 1, morris(x,y)) +
(qif use2(x-1,morris(x,y)) qthen cm(x,y) + 1 qelse 0) +1%1

	A second example comes from

	%2tak(x,y,z) ← qif x lesseq y qthen y qelse tak(tak(x-1,y,z),tak(y-1,z,x),
tak(z-1,x,y))%2

and is

	%2ctak(x,y,z) ← qif x lesseq y qthen 0 qelse ctak(tak(x-1,y,z),
tak(y-1,z,x),tak(z-1,x,y)) + 
(qif use1(tak(x-1,y,z),tak(y-1,z,x),tak(z-1,x,y)) qthen ctak(x-1,y,z) qelse 0)
+ (qelse qif use2(tak(x-1,y,z),tak(y-1,z,x),tak(z-1,x,y)) qthen ctak(y-1,z,x) qelse 0)
+ (qelse qif use3(tak(x-1,y,z),tak(y-1,z,x),tak(z-1,x,y)) qthen ctak(z-1,x,y) qelse 0)

where

	%2use1(x,y,z) = T

	%2use2(x,y,z) = T

	%2use3(x,y,z) ← qif x lesseq y qthen F qelse
(use1(tak(x-1,y,z),tak(y-1,z,x),tak(z-1,x,y)) and use3(x-1,y,z))
or (use2( ... ) and use2(y-1,z,x))
or (use3( ... ) and use1(z-1,x,y)).